D:Dsys, i:Id, s:M(i).state. stutter-state(s)  d-world-state(D;i) 

latex

Definitions	M.state, Dsys, d-world-state(D;i), stutter-state(s), null, d-decl(D;i), M.Msg, M(i), Id, source(l), mlnk(m), x:A. B(x), t  T
Lemmas	mlnk wf d, lsrc wf, ma-msg wf, d-decl wf, null-action wf, dsys wf, Id wf, d-m wf, ma-st wf